Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Isabelle/HOL translation: records and named patterns #2963

Merged
merged 17 commits into from
Aug 29, 2024
Merged

Isabelle/HOL translation: records and named patterns #2963

merged 17 commits into from
Aug 29, 2024

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Aug 19, 2024 •
edited
Loading

Checklist

  • record creation
  • record projections
  • record update
  • top-level record patterns
  • nested record patterns
  • named patterns
  • remove redundant pattern matching clauses
  • remove redundant single-branch pattern matches

@lukaszcz lukaszcz added this to the 0.6.6 milestone Aug 19, 2024
@lukaszcz lukaszcz self-assigned this Aug 19, 2024
@lukaszcz lukaszcz force-pushed the isabelle-records branch 2 times, most recently from f82cf71 to 23585b0 Compare August 20, 2024 18:32
@lukaszcz lukaszcz changed the title Isabelle/HOL translation: records Isabelle/HOL translation: records and named patterns Aug 21, 2024
@lukaszcz lukaszcz marked this pull request as ready for review August 23, 2024 10:06
@lukaszcz lukaszcz mentioned this pull request Aug 27, 2024
Merged
@lukaszcz lukaszcz added the enhancement New feature or request label Aug 28, 2024
janmasrovira
janmasrovira previously approved these changes Aug 29, 2024
View reviewed changes
src/Juvix/Compiler/Backend/Isabelle/Extra.hs Outdated Show resolved Hide resolved
src/Juvix/Compiler/Backend/Isabelle/Extra.hs Outdated Show resolved Hide resolved
src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
Comment on lines +704 to +705
getRecordUpdate :: Internal.Application -> Maybe (Name, [Name], Internal.Expression, [(Name, Internal.Expression)])
getRecordUpdate Internal.Application {..} = case _appLeft of
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nesting makes this a bit hard to read

@lukaszcz @janmasrovira
Update src/Juvix/Compiler/Backend/Isabelle/Extra.hs
7fd84c5 
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
@lukaszcz @janmasrovira
Update src/Juvix/Compiler/Backend/Isabelle/Extra.hs
745f0db 
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
@lukaszcz lukaszcz merged commit a4f3704 into main Aug 29, 2024
4 checks passed
@lukaszcz lukaszcz deleted the isabelle-records branch August 29, 2024 14:16
lukaszcz added a commit that referenced this pull request Sep 2, 2024
@lukaszcz @janmasrovira
Isabelle/HOL translation: comments (#2974)
b9d8641 
* Closes #2962 
* Depends on #2963 
* In Isabelle/HOL comments cannot appear in internal syntax. All
comments inside a Juvix definition are moved outside: to before the
definition or before the earliest function clause.

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@janmasrovira janmasrovira janmasrovira approved these changes

@paulcadman paulcadman Awaiting requested review from paulcadman

@jonaprieto jonaprieto Awaiting requested review from jonaprieto

Assignees

@lukaszcz lukaszcz

Labels
enhancement New feature or request isabelle
Projects
None yet
Milestone
0.6.6
2 participants
@lukaszcz @janmasrovira